COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	addon[w86,jmc]		Solutions are add-ons to problem statements
C00007 ENDMK
C⊗;
addon[w86,jmc]		Solutions are add-ons to problem statements

	Suppose a person  A  states a problem  p,  and another person  B  solves
it and tells  A  the solution  s.  As far as  A   is concerned, the language
of the solution is an add-on to the statement of the problem.  We
want to formalize this relation between the solution and the problem.
We begin with the problem of coloring a map with four colors.  We will
use set theory as our language, because it seems appropriate and
maybe even necessary from this general point of view.

	Consider the formula

	(∀ S n)(okmap(S,n) ≡ n ε 2↑(S x S) ∧ (∀ x y)(n(x,y) = n(y,x))).

Our intent is that  S  is the set of countries and  n  is the adjacency
or ``nextness'' relation.  However, the formula can stand by itself in the
language of set theory as the definition of a map as a symmetric relation
on the set of countries.

	Now consider the further formula

	(∀S n C f)(coloring(S,n,C,f) ≡ okmap(S,n) 
		∧ f ε C↑S ∧ (∀x y)(n(x,y) = 1 ⊃ f(x) ≠ f(y)).

The intent here is that  C  is the set of colors and  f  assigns colors
to countries and the formula states that adjacent countries have
different colors.

We can consider an even more abstract formulation,

	∀M.ismap(M) ≡ ∃S n.M=<S,n> ∧ okmap(S,n)

and

∀M F.iscoloring(M,F) ≡ ismap(M) ∧ ∃C f.F=<C,f> ∧ coloring(S*(M),n*(M),C,f).

This isn't entirely consistent as stated, since in the second formula
S* and n* are taken as functions of M.  I'll figure out how to resolve
this later.  On the one hand it seems desirable to have formulas
that can be interprets as saying ``M is a map iff \ldots'' and
``F is a coloring of M iff ...'', and on the other hand, describing
these relations requires referring to the countries and adjacency
relation of M.  For now we'll use the original formulation that
refers to S and m, but it may be necessary in the long run to go
on to using M.

	A solution to the problem is given by a function that gives
the coloring map  f  in terms of  S,  n  and  C.  Thus we want a
relation that says

∀S n C.easilyColored(S,n,C,a) 
		⊃ coloring(S,n,C,extension(ColoringAlgorithm(S,n,C,a)))
			∧ good(ColoringAlgorithm,S,n,C,a)

Where the predicate  easilyColored  includes conditions like
planarity and has the extra argument  a  that includes such
information as enumerations
of the countries and the presentation of the adjacency relation.

The point of the example, which needs to be spelled out with the
details of  easilyColored   and  ColoringAlgorithm  is that the algorith
needs to be presented as a function of the arguments explicitly given.
Later improvements to the algorithm need to be presented as functions
of the algorithm or else we need to admit that the algorithm isn't
being improved but the problem is being solved again.  More generally,
we need to formalize the notion of improvement in terms of a relation
between what is being improved, the original problem, and the
original solution.